\begin{tabbing}
es{-}pstar{-}q(${\it es}$;$a$,$b$.$p$($a$;$b$);$a$,$b$.$q$($a$;$b$);$e_{1}$;$e_{2}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\exists$$m$:$\mathbb{N}^{+}$, $f$:(\{0..$m$$^{-}$\}$\rightarrow$\{$e$:es{-}E(${\it es}$)$\mid$ es{-}loc(${\it es}$; $e$) $=$ es{-}loc(${\it es}$; $e_{1}$) $\in$ Id \}).\+
\\[0ex]$f$(0) $=$ $e_{1}$ $\in$ es{-}E(${\it es}$) \& es{-}le(${\it es}$;$f$($m$$-$1);$e_{2}$)
\\[0ex]\& ($\forall$$i$:\{0..($m$$-$1)$^{-}$\}. es{-}locl(${\it es}$; ($f$($i$)); ($f$($i$+1))))
\\[0ex]\& ($\forall$$i$:\{0..($m$$-$1)$^{-}$\}. $p$($f$($i$);es{-}pred(${\it es}$; ($f$($i$+1)))))
\\[0ex]\& $q$($f$($m$$-$1);$e_{2}$)
\-
\end{tabbing}